/*@ true */
int  foo()
{
  int  ii;


  ii=0;
  return (ii);
}
/*@ true */


/*@ true */
int  main()
{
  int  i;
  int  j;
  int  k;


  i=9999;
  k=(2) + (i);
  while ((3) < (i))    /*@ true */
  {
    i=(i) - (1);
  }
  return (9);
}
/*@ true */


